\begin{tabbing}
pre{-}p(${\it es}$;$i$;${\it ds}$;$a$;$T$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; $i$; $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.\=es{-}kind(${\it es}$; $e$) $=$ locl($a$) $\in$ Knd\+\+
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$ \& $P$(es{-}state{-}when(${\it es}$;$e$),es{-}val(${\it es}$; $e$)))
\-\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.existse{-}ge(${\it es}$;$e$;${\it e'}$.es{-}kind(${\it es}$; ${\it e'}$) $=$ locl($a$) $\in$ Knd\+
\\[0ex]$\vee$ ($\forall$$v$:$T$. $\neg$$P$(es{-}state{-}after(${\it es}$;${\it e'}$),$v$))))
\-\\[0ex]\& (($\exists$$v$:$T$. $P$(es\_init(${\it es}$)($i$),$v$)) $\Rightarrow$ ($\exists$$e$:es{-}E(${\it es}$). es{-}loc(${\it es}$; $e$) $=$ $i$ $\in$ Id))
\-\-
\end{tabbing}